active1(c) -> mark1(f1(g1(c)))
active1(f1(g1(X))) -> mark1(g1(X))
proper1(c) -> ok1(c)
proper1(f1(X)) -> f1(proper1(X))
proper1(g1(X)) -> g1(proper1(X))
f1(ok1(X)) -> ok1(f1(X))
g1(ok1(X)) -> ok1(g1(X))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
↳ QTRS
↳ DependencyPairsProof
active1(c) -> mark1(f1(g1(c)))
active1(f1(g1(X))) -> mark1(g1(X))
proper1(c) -> ok1(c)
proper1(f1(X)) -> f1(proper1(X))
proper1(g1(X)) -> g1(proper1(X))
f1(ok1(X)) -> ok1(f1(X))
g1(ok1(X)) -> ok1(g1(X))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
TOP1(mark1(X)) -> PROPER1(X)
PROPER1(g1(X)) -> G1(proper1(X))
PROPER1(g1(X)) -> PROPER1(X)
PROPER1(f1(X)) -> PROPER1(X)
TOP1(ok1(X)) -> TOP1(active1(X))
ACTIVE1(c) -> F1(g1(c))
F1(ok1(X)) -> F1(X)
TOP1(mark1(X)) -> TOP1(proper1(X))
G1(ok1(X)) -> G1(X)
ACTIVE1(c) -> G1(c)
TOP1(ok1(X)) -> ACTIVE1(X)
PROPER1(f1(X)) -> F1(proper1(X))
active1(c) -> mark1(f1(g1(c)))
active1(f1(g1(X))) -> mark1(g1(X))
proper1(c) -> ok1(c)
proper1(f1(X)) -> f1(proper1(X))
proper1(g1(X)) -> g1(proper1(X))
f1(ok1(X)) -> ok1(f1(X))
g1(ok1(X)) -> ok1(g1(X))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
TOP1(mark1(X)) -> PROPER1(X)
PROPER1(g1(X)) -> G1(proper1(X))
PROPER1(g1(X)) -> PROPER1(X)
PROPER1(f1(X)) -> PROPER1(X)
TOP1(ok1(X)) -> TOP1(active1(X))
ACTIVE1(c) -> F1(g1(c))
F1(ok1(X)) -> F1(X)
TOP1(mark1(X)) -> TOP1(proper1(X))
G1(ok1(X)) -> G1(X)
ACTIVE1(c) -> G1(c)
TOP1(ok1(X)) -> ACTIVE1(X)
PROPER1(f1(X)) -> F1(proper1(X))
active1(c) -> mark1(f1(g1(c)))
active1(f1(g1(X))) -> mark1(g1(X))
proper1(c) -> ok1(c)
proper1(f1(X)) -> f1(proper1(X))
proper1(g1(X)) -> g1(proper1(X))
f1(ok1(X)) -> ok1(f1(X))
g1(ok1(X)) -> ok1(g1(X))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
G1(ok1(X)) -> G1(X)
active1(c) -> mark1(f1(g1(c)))
active1(f1(g1(X))) -> mark1(g1(X))
proper1(c) -> ok1(c)
proper1(f1(X)) -> f1(proper1(X))
proper1(g1(X)) -> g1(proper1(X))
f1(ok1(X)) -> ok1(f1(X))
g1(ok1(X)) -> ok1(g1(X))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G1(ok1(X)) -> G1(X)
POL(G1(x1)) = x1
POL(ok1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
active1(c) -> mark1(f1(g1(c)))
active1(f1(g1(X))) -> mark1(g1(X))
proper1(c) -> ok1(c)
proper1(f1(X)) -> f1(proper1(X))
proper1(g1(X)) -> g1(proper1(X))
f1(ok1(X)) -> ok1(f1(X))
g1(ok1(X)) -> ok1(g1(X))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
F1(ok1(X)) -> F1(X)
active1(c) -> mark1(f1(g1(c)))
active1(f1(g1(X))) -> mark1(g1(X))
proper1(c) -> ok1(c)
proper1(f1(X)) -> f1(proper1(X))
proper1(g1(X)) -> g1(proper1(X))
f1(ok1(X)) -> ok1(f1(X))
g1(ok1(X)) -> ok1(g1(X))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F1(ok1(X)) -> F1(X)
POL(F1(x1)) = x1
POL(ok1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
active1(c) -> mark1(f1(g1(c)))
active1(f1(g1(X))) -> mark1(g1(X))
proper1(c) -> ok1(c)
proper1(f1(X)) -> f1(proper1(X))
proper1(g1(X)) -> g1(proper1(X))
f1(ok1(X)) -> ok1(f1(X))
g1(ok1(X)) -> ok1(g1(X))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
PROPER1(g1(X)) -> PROPER1(X)
PROPER1(f1(X)) -> PROPER1(X)
active1(c) -> mark1(f1(g1(c)))
active1(f1(g1(X))) -> mark1(g1(X))
proper1(c) -> ok1(c)
proper1(f1(X)) -> f1(proper1(X))
proper1(g1(X)) -> g1(proper1(X))
f1(ok1(X)) -> ok1(f1(X))
g1(ok1(X)) -> ok1(g1(X))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PROPER1(g1(X)) -> PROPER1(X)
PROPER1(f1(X)) -> PROPER1(X)
POL(PROPER1(x1)) = 3·x1
POL(f1(x1)) = 3 + 2·x1
POL(g1(x1)) = 3 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
active1(c) -> mark1(f1(g1(c)))
active1(f1(g1(X))) -> mark1(g1(X))
proper1(c) -> ok1(c)
proper1(f1(X)) -> f1(proper1(X))
proper1(g1(X)) -> g1(proper1(X))
f1(ok1(X)) -> ok1(f1(X))
g1(ok1(X)) -> ok1(g1(X))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
TOP1(ok1(X)) -> TOP1(active1(X))
TOP1(mark1(X)) -> TOP1(proper1(X))
active1(c) -> mark1(f1(g1(c)))
active1(f1(g1(X))) -> mark1(g1(X))
proper1(c) -> ok1(c)
proper1(f1(X)) -> f1(proper1(X))
proper1(g1(X)) -> g1(proper1(X))
f1(ok1(X)) -> ok1(f1(X))
g1(ok1(X)) -> ok1(g1(X))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TOP1(mark1(X)) -> TOP1(proper1(X))
Used ordering: Polynomial interpretation [21]:
TOP1(ok1(X)) -> TOP1(active1(X))
POL(TOP1(x1)) = x1
POL(active1(x1)) = x1
POL(c) = 3
POL(f1(x1)) = 1
POL(g1(x1)) = 0
POL(mark1(x1)) = 1 + 2·x1
POL(ok1(x1)) = x1
POL(proper1(x1)) = 2·x1
proper1(f1(X)) -> f1(proper1(X))
g1(ok1(X)) -> ok1(g1(X))
active1(f1(g1(X))) -> mark1(g1(X))
proper1(c) -> ok1(c)
proper1(g1(X)) -> g1(proper1(X))
f1(ok1(X)) -> ok1(f1(X))
active1(c) -> mark1(f1(g1(c)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
TOP1(ok1(X)) -> TOP1(active1(X))
active1(c) -> mark1(f1(g1(c)))
active1(f1(g1(X))) -> mark1(g1(X))
proper1(c) -> ok1(c)
proper1(f1(X)) -> f1(proper1(X))
proper1(g1(X)) -> g1(proper1(X))
f1(ok1(X)) -> ok1(f1(X))
g1(ok1(X)) -> ok1(g1(X))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TOP1(ok1(X)) -> TOP1(active1(X))
POL(TOP1(x1)) = 3·x1
POL(active1(x1)) = 1 + x1
POL(c) = 3
POL(f1(x1)) = 1 + 2·x1
POL(g1(x1)) = 3 + 2·x1
POL(mark1(x1)) = 1
POL(ok1(x1)) = 3 + 2·x1
active1(f1(g1(X))) -> mark1(g1(X))
active1(c) -> mark1(f1(g1(c)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
active1(c) -> mark1(f1(g1(c)))
active1(f1(g1(X))) -> mark1(g1(X))
proper1(c) -> ok1(c)
proper1(f1(X)) -> f1(proper1(X))
proper1(g1(X)) -> g1(proper1(X))
f1(ok1(X)) -> ok1(f1(X))
g1(ok1(X)) -> ok1(g1(X))
top1(mark1(X)) -> top1(proper1(X))
top1(ok1(X)) -> top1(active1(X))